 27 Jul, 2016 1 commit


Robbert Krebbers authored
This makes type checking more directed, and somewhat more predictable. On the downside, it makes it impossible to declare the singleton on lists as an instance of SingletonM and the insert and alter operations on functions as instances of Alter and Insert. However, these were not used often anyway.

 30 Jun, 2016 1 commit


JacquesHenri Jourdan authored

 27 May, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 22 May, 2016 2 commits


Robbert Krebbers authored
Initial commit by Amin Timany.

Robbert Krebbers authored

 30 Mar, 2016 1 commit


Robbert Krebbers authored
This seems to shorten type class search.

 21 Mar, 2016 1 commit


Robbert Krebbers authored
Also, slightly reorganize.

 04 Mar, 2016 1 commit


Robbert Krebbers authored

 03 Mar, 2016 1 commit


Robbert Krebbers authored

 20 Feb, 2016 2 commits
 17 Feb, 2016 2 commits


Robbert Krebbers authored
simplify_equality => simplify_eq simplify_equality' => simplify_eq/= simplify_map_equality => simplify_map_eq simplify_map_equality' => simplify_map_eq/= simplify_option_equality => simplify_option_eq simplify_list_equality => simplify_list_eq f_equal' => f_equal/= The /= suffixes (meaning: do simpl) are inspired by ssreflect.

Robbert Krebbers authored

 13 Feb, 2016 2 commits


Robbert Krebbers authored
Also, make our redefinition of done more robust under different orders of Importing modules.

Robbert Krebbers authored
Since Coq 8.4 did not backtrack on eauto premises, we used to ensure that hints like Hint Extern 0 (?x ≡{_}≡ ?y) => reflexivity. were not used for goals involving evars by writing ?x ≡{_}≡ ?y instead of _ ≡{_}≡ _. This seems to be a legacy issue that no longer applies to Coq 8.5, so I have removed these restrictions making these hints thus more powerful.

 11 Feb, 2016 1 commit


Robbert Krebbers authored
Also do some minor clean up.

 20 Jan, 2016 1 commit


Robbert Krebbers authored
And use more uniform variable names.

 12 Jan, 2016 1 commit


Robbert Krebbers authored

 15 Dec, 2015 1 commit


Robbert Krebbers authored

 18 Nov, 2015 1 commit


Robbert Krebbers authored

 16 Nov, 2015 1 commit


Robbert Krebbers authored

 11 Nov, 2015 1 commit


Robbert Krebbers authored

 01 Feb, 2017 1 commit


Robbert Krebbers authored
The port makes the following notable changes: * The carrier types of separation algebras and integer environments are no longer in Set. Now they have a type at a fixed type level above Set. This both works better in 8.5 and makes the formalization more general. I have tried putting them at polymorphic type levels, but that increased the compilation time by an order of magnitude. * I am using a custom f_equal tactic written in Ltac to circumvent bug #4069. That bug has been fixed, so this custom tactic can be removed when the next beta of 8.5 is out.

 04 Jun, 2015 1 commit


Robbert Krebbers authored

 25 Feb, 2015 1 commit


Robbert Krebbers authored

 16 Feb, 2015 1 commit


Robbert Krebbers authored

 08 Feb, 2015 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
Important changes in the core semantics: * Types extended with function types. Since function types are a special kind of pointer types, types now have an additional mutual part called "ptr_type". * Pointers extended with function pointers. Theses are just names that refer to an actual function in the function environment. * Typing environments extended to assign argument and return types to function names. Before we used a separate environment for these, but since the argument and return types are already needed to type function pointers, this environment would appear in pretty much every typing judgment. As a sideeffect, the frontend has been rewritten entirely. The important changes are: * Type checking of expressions is more involved: there is a special kind of expression type corresponding to a function designator. * To handle things like block scoped extern function, more statefullness was needed. To prepare for future extensions, the entire frontend now uses a state monad.

 29 Jan, 2015 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
addresses. The operation "mem_force Γ m a" used to apply the identify function to pricisely the object "a", even in case "a" is an "unsigned char" address refering to an individual byte. This caused the ctree substructure of the entire subobject to disappear and had the undesired effect that: mem_force Γ a m ⊑{Γ,true@Γm} m failed to hold (i.e. unused reads cannot be removed).

 25 Jan, 2015 1 commit


Robbert Krebbers authored

 16 Dec, 2014 1 commit


Robbert Krebbers authored
The refinement relation on addresses allows union references to be refined: (β2 → β1) → RUnion i s β1 ⊆ RUnion i s β2 The result is that frozen values are below their unfrozen variant, which made it possible to prove that constant propagation (see constant_propagation.v) can be performed on the level of the memory model.

 30 Sep, 2014 1 commit


Robbert Krebbers authored
Now it only performs injection on hypotheses of the shape f .. = f ..

 24 Sep, 2014 1 commit


Robbert Krebbers authored

 06 Sep, 2014 1 commit


Robbert Krebbers authored

 03 Sep, 2014 1 commit


Robbert Krebbers authored

 06 Aug, 2014 1 commit


Robbert Krebbers authored

 10 Jul, 2014 1 commit


Robbert Krebbers authored

 25 Jun, 2014 1 commit


Robbert Krebbers authored
* Equality comparison of NULL and non NULL pointers should be defined * Pointer comparisons, casts, and truth should only be defined for pointers that are alive * Treat dead pointers as indeterminate values in refinements. The proofs that all operations preserve refinement indicate that dead pointers can be indeed by replaced by anything without affecting the program's behavior.
