--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on October 2009 ---
Here is the C source file: -------------------------------------------------- int S=0; int T[5]; int main(void) { int i; int *p = &T[0] ; for (i=0; i<5; i++) { S = S+i; *p++ = S; } return S; } -------------------------------------------------- and the first.jc --------------------------------------------------------------- # IntModel = bounded # InvariantPolicy = Arguments # SeparationPolicy = Regions # AnnotationPolicy = None # AbstractDomain = Pol axiomatic Padding { logic type padding } type int32 = -2147483648..2147483647 type int8 = -128..127 tag int_P = { int32 int_M: 32; } type int_P = [int_P] tag char_P = { int8 char_M: 8; } type char_P = [char_P] tag void_P = { } type void_P = [void_P] unit __globinit_whole_program() behavior default: assumes true; ensures (C_1 : true); ; int32 S; int_P[0..4] T; invariant valid_T : ((\offset_min(T) <= 0) && (\offset_max(T) >= 4)) int32 main() behavior default: assumes true; ensures (C_16 : true); { (var int32 i); (var int_P[..] p); (var int_P[..] tmp); { (C_2 : __globinit_whole_program()); (C_3 : (p = T)); (C_4 : (i = 0)); { loop while (true) { { (if (i < 5) then () else (goto while_0_break)); (C_7 : (S = (C_6 : ((C_5 : (S + i)) :> int32)))); { { (C_8 : (tmp = p)); (C_10 : (p = (C_9 : (p + 1)))) }; (C_12 : ((C_11 : tmp.int_M) = S)) }; (C_15 : (i = (C_14 : ((C_13 : (i + 1)) :> int32)))) } }; (while_0_break : ()) }; (return S) } } --------------------------------------------------------------- 2009/10/14 Hollas Boris (CR/AEY1) <Boris.Hollas at de.bosch.com> > Post you source file. > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091014/39683234/attachment.htm