--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on January 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Verification of integer and pointer programs



Hello and happy new year everyone!

I had a look at Yannik Moy's thesis to find out how integer and pointer programs are verified. However, some things are not yet clear to me.

- Suppose there's a pointer expression *(expr) in a statement, where expr evaluates to a memory location. Is then an implicit precondition \valid(expr) generated?
- For an assignment x=e to an int x, is an implicit precondition min_int <= e <= max_int generated?
- In this case, are the rules for the wp-calculus changed accordingly? Eg, for a variable x and an expression e containing pointer expressions, is

  wp(x=e, Q) = Q[ x -> e] \cup \bigcup_p {\valid(p)} \cup {min_int <= e <= max_int}

  the rule for assignment, where p ranges over all pointer expressions *(expr) in e?

-Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100114/673ab110/attachment.htm