--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on October 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ARe: jessie problem



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