Re: longest path through a task

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

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
       .      @       .