- 16 Feb, 2016 2 commits
-
-
Robbert Krebbers authored
-
Ralf Jung 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.
-
- 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 side-effect, 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 state-fullness 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 r-value of pointer type instead of an l-value. * The executable semantics for expressions is now non-deterministic. 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 l-values instead of r-values. 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
-