--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on May 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Set global variables uninitialized at Value analysis start



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