From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: buffer2.nntp.dca1.giganews.com!border2.nntp.dca1.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!1.eu.feeder.erje.net!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: longest path through a task Date: Fri, 29 May 2015 07:38:37 +0300 Organization: Tidorum Ltd Message-ID: References: <9ad1fcdc-cdf9-4ff0-aa7e-051d53b6736a@googlegroups.com> <7d56e720-5e91-4950-b4ae-29d7ddbdc11a@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net oJVc989Y8HaaGuRmjAB1HQKftHcNw17GfizsKH1waybkQnYz1b Cancel-Lock: sha1:2MzrVlnbXWMaG698vwQWl4600eo= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:31.0) Gecko/20100101 Thunderbird/31.7.0 In-Reply-To: Xref: number.nntp.giganews.com comp.lang.ada:193355 Date: 2015-05-29T07:38:37+03:00 List-Id: On 15-05-28 16:04 , jan.de.kruyf@gmail.com wrote: > That is sad. But if you did not shoot, you would have missed also. Yeah, but perhaps I could have taken better aim... I did have a couple of moments of euphoria, feeling the freedom of the entrepreneur :-) > Does Bound-T eat Thumb-2 code you think? I was working on that at the time when it became clear that Bound-T would not make it as a commercial product. I still have hopes of finishing a Bound-T version for the Cortex M-series, but my employer loves me so much that I have no time... The main problem is that the way Bound-T analyses the computation and data flow in the code is (intentionally) unsound (in the program-proving sense). For example, pointers are mainly ignored, and there is no global value analysis (which would be required for most pointer analysis). This was not so harmful at the start (some 15 years ago, gosh) when the analysis results were not used for much (mainly to find iteration bounds on simple loops) but by and by the use of the analysis results expanded (sometimes by technical necessity) to include, for example, detection of infeasible execution paths -- and if that is based on an unsound analysis, it is very likely that an analysis of a large program will trigger some false conclusions, and the end results of the analysis will be wrong. So Bound-T unfortunaly needs a fresh start with respect to the model of the computation. I have been thinking about that for a good while, but I haven't found anything good yet. The simple and sound methods are so much weaker than the current model that is based on a Presburger Arithmetic and the Omega library. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .