--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on January 2010 ---
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