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] Set global variables uninitialized at Value analysis start

  • Subject: [Frama-c-discuss] Set global variables uninitialized at Value analysis start
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Wed, 29 May 2013 14:01:13 +0200
  • In-reply-to: <CAC3Lx=brLLEht0LqH7TMdTvexPKExjpS+btJcWc60mCup_rtFA@mail.gmail.com>
  • References: <CAC3Lx=Zzm7DFwU_XEtn+u_p=18kgn-qFRQMp5VOpBqRs8PDZAw@mail.gmail.com> <E50756B2-BF80-4A38-AE62-AD3F4A70A264@cea.fr> <CAC3Lx=ZT5n1iZ-oJZHGr2emVsNRd2HgoSaC+Tghn69Cj=UR0eA@mail.gmail.com> <CAC3Lx=brLLEht0LqH7TMdTvexPKExjpS+btJcWc60mCup_rtFA@mail.gmail.com>
Hello David,

On Mon, May 27, 2013 at 4:39 PM, David MENTRE <dmentre at linux-france.org> wrote:
>       match typ with
>       | TInt _ | TEnum (_, _)->
>           bind_entire_loc Cvalue.V_Or_Uninitialized.uninitialized
> """
>
> Above code does not compile because a value of type Cvalue.V.t is
> expected and "uninitialized" is of type
> "Cvalue.V_Or_Uninitialized.un_t".

The programmatic approach would be to replace all the relevant calls to
  bind_entire_loc loc v
by
  Cvalue.Model.add_binding_not_initialized state loc
(In each case of the matching you found in initial_state)

However, I cannot guarantee the correctness of the result in all
corner cases, since we never use this mode. For example, variables
with an intializer are still discarded. The non-programmatic approach
proposed by Pascal is probably a safer bet.

--
Boris