--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on May 2013 ---
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