Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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