 13 Feb, 2016 1 commit


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.

 10 Feb, 2016 1 commit


Ralf Jung authored

 16 Jan, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
These are hardly used, and confusing since we have so many operations of different arities that distribute.

 12 Jan, 2016 1 commit


Robbert Krebbers authored

 21 Dec, 2015 1 commit


Robbert Krebbers authored

 15 Dec, 2015 1 commit


Robbert Krebbers authored

 19 Nov, 2015 1 commit


Robbert Krebbers authored

 18 Nov, 2015 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 17 Nov, 2015 1 commit


Robbert Krebbers authored

 16 Nov, 2015 1 commit


Robbert Krebbers authored

 03 Feb, 2017 1 commit


Robbert Krebbers authored

 01 Feb, 2017 2 commits


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.

Robbert Krebbers authored

 10 Jun, 2015 1 commit


Robbert Krebbers authored

 25 Feb, 2015 1 commit


Robbert Krebbers authored

 13 Feb, 2015 1 commit


Robbert Krebbers authored
Ported from popl2014 branch.

 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.

 27 Jan, 2015 1 commit


Robbert Krebbers authored
* This behavior is "implementation defined" and can be turned on and off using the Boolean field "alloc_can_fail" of the class "Env". * The expression "EAlloc" is now an rvalue of pointer type instead of an lvalue. * The executable semantics for expressions is now nondeterministic. Hence, some proofs had to be revised.

 25 Jan, 2015 1 commit


Robbert Krebbers authored

 15 Nov, 2014 1 commit


Robbert Krebbers authored
Integers with the same size, are no longer supposed to have the same rank. As a result, the C integer types (char, short, int, long, long long) are different (and thus cannot alias) even if they have the same size. We now have to use a more involved definition of integer promotions and usual arithmetic conversions. However, this new definition follows the C standard literally.

 08 Oct, 2014 1 commit


Robbert Krebbers authored
Memory refinements now carry a boolean parameter that has the following meaning: [false] : Behave like a simple renaming of memories that merely allows to permute object identifiers. It does not allow to refine memories into a more defined version. [true] : Behave like before. Objects can be injected, and memory contents can be refined into a more defined variant. We make refinements parametric in these two variant to avoid code duplication, and because the [false] variant is a special case of the [true] variant. For completeness of the executable semantics, we now use the [false] variant.

 30 Sep, 2014 1 commit


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

 25 Aug, 2014 1 commit


Robbert Krebbers authored

 23 Jun, 2014 1 commit


Robbert Krebbers authored

 17 Jun, 2014 1 commit


Robbert Krebbers authored
variables.

 16 Jun, 2014 1 commit


Robbert Krebbers authored
Major changes: * Make void a base type, and include a proper void base value. This is necessary because expressions (free, functions without return value) can yield a void. We now also allow void casts conforming to the C standard. * Various missing lemmas about typing, weakening, decidability, ... * The operations "free" and "alloc" now operate on lvalues instead of rvalues. This removes some duplication. * Improve notations of expressions and statements. Change the presence of the operators conforming to the C standard. Small changes: * Use the classes "Typed" and "TypeCheck" for validity of indexes in memory. This gives more uniform notations. * New tactic "typed_inversion" performs inversion on an inductive predicate of type "Typed" and folds the premises. * Remove a horrible hack in the definitions of the classes "FMap", "MBind", "OMap", "Alter" that was used to let "simpl" behave better. Instead, we have defined a tactic "csimpl" that folds the results after performing an ordinary "simpl". * Fast operation to remove duplicates from lists using hashsets. * Make various type constructors (mainly finite map implementations) universe polymorphic by packing them into an inductive. This way, the whole C syntax can live in type, avoiding the need for (slow) universe checks.

 05 Jun, 2014 1 commit


Robbert Krebbers authored
Major changes: * A data structure to collect locked addresses in memory. * Operations to lock and unlock addresses. * Remove [ctree_Forall] and express it using [Forall] and [ctree_flatten]. This saves a lot of lines of code. * Add a [void] value. This value cannot be typed, but will be used as a dummy return value for functions with return type [void]. Minor changes: * Various deciders in preparation of the executable semantics. * Improve naming and notations. * Remove obsolete stuff.

 02 May, 2014 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 09 Sep, 2013 1 commit


Robbert Krebbers authored

 21 Aug, 2013 1 commit


Robbert Krebbers authored

 12 Aug, 2013 1 commit


Robbert Krebbers authored
This commit includes the following changes: * More theorems about pre, partial and total orders. * Define the lexicographic order on various commonly used data types. * Mergesort and its correctness proof. * Implement finite maps and sets using ordered association lists.

 17 Jun, 2013 1 commit


Robbert Krebbers authored

 07 May, 2013 1 commit


Robbert Krebbers authored
The refactoring includes: * Use infix notations for the various list relations * More consistent naming * Put lemmas on one line whenever possible * Change proofs into oneliners when possible * Make better use of the "Implicit Types" command * Improve the order of the list module by placing all definitions at the start, then the proofs, and finally the tactics. Besides, there is some new machinery for proofs by reflection on lists. It is used for a decision procedure for permutations and list containment.

 02 Apr, 2013 1 commit


Robbert Krebbers authored

 14 Mar, 2013 1 commit


Robbert Krebbers authored
