diff options
Diffstat (limited to 'cfrontend/Initializersproof.v')
| -rw-r--r-- | cfrontend/Initializersproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 5db4718..b6fc728 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -680,7 +680,7 @@ Qed. (** A semantics for general initializers *) -Definition dummy_function := mkfunction Tvoid nil nil Sskip. +Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip. Fixpoint fields_of_struct (id: ident) (ty: type) (fl: fieldlist) (pos: Z) : list (Z * type) := match fl with |