aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-1033-1327/+1365
|\
| * coq 8.13.2David Monniaux2021-06-071-2/+1
| |
| * [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-0131-144/+155
| | | | | | | | cfrontend/C2C.ml
| * replacing omega with lia in some fileLéo Gourdin2021-03-292-32/+34
| |
| * Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2315-1150/+1176
| |\ | | | | | | | | | | | | | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| | * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-213-33/+36
| | | | | | | | | | | | | | | | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
| | * Define `fold_ind_aux` and `fold_ind` transparentlyXavier Leroy2021-01-211-2/+2
| | | | | | | | | | | | | | | | | | The extraction mechanism wants to extract them (because they are in Type, probably). The current opaque definition causes a warning at extraction-time.
| | * Add new fold_ind induction principle for foldsXavier Leroy2021-01-131-63/+82
| | | | | | | | | | | | | | | | | | | | | fold_inv is in Type, hence can prove goals such as `{ x | P x }`. Also, no extensionality property is needed. fold_rec is now derived from fold_inv.
| | * Add lemma list_norepet_revXavier Leroy2021-01-131-0/+8
| | |
| | * Replace `omega` tactic with `lia`Xavier Leroy2020-12-2914-1026/+1022
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
| | * Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-292-13/+13
| | | | | | | | | | | | | | | | | | | | | | | | | | | IEEE754_extra: clear unused context so that none of the context is picked up by tactics and ends as extra parameters to theorems int_round_odd_bits and int_round_odd_le Floats: simplify uses of int_round_odd_bits and int_round_odd_le accordingly.
* | | better autodestruct ?Sylvain Boulmé2021-05-111-1/+16
| | |
* | | start the new "BTL" IR.Sylvain Boulmé2021-04-281-0/+6
|/ /
* | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-072-0/+50
| |
* | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-177-10/+279
|\ \
| * \ Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0417-10/+1710
| |\ \ | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * \ \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-187-10/+279
| |\ \ \ | | | |/ | | |/|
| | * | Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-212-4/+3
| | | | | | | | | | | | | | | | configure flags -use-external-Flocq and -use external-MenhirLib.
| | * | Simplify two scripts in Zbits (#369)Maxime Dénès2020-09-181-2/+2
| | | | | | | | | | | | | | | | | | | | Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity.
| | * | Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | | | | | | | | | | | | | | | | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
| | * | Add a canonical encoding of identifiers as numbers and use it in clightgen ↵Xavier Leroy2020-05-191-3/+76
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (#353) Within CompCert, identifiers (names of C functions, variables, types, etc) are represented by unique positive numbers, sometimes called "atoms". In the original implementation, atoms 1, 2, ..., N are assigned to identifiers as they are encountered. The resulting number are small and are efficient when used as keys in data structures such as PTrees. However, the mapping from C source-level identifiers to atoms differs between compilation units. This is not a problem for CompCert but complicates CompCert-based verification tools that need to combine several compilation units. This commit introduces an alternate implementation of atoms, suggested by Andrew Appel. The choice between implementations is governed by the Boolean reference `Camlcoq.use_canonical_atoms`. In the alternate implementation, identifiers are converted to bit sequences via a Huffman encoding, then the bits are represented as positive numbers. The same identifier is always represented by the same number. However, the numbers are usually bigger than in the original implementation, making PTree operations slower: lookups and updates take time linear in the length of the identifier, instead of logarithmic time in the number of identifiers encountered. The CompCert compiler (the `ccomp` executable) still uses the original implementation, but the `clightgen` tool used in conjunction with the VST program logic can use either implementations: - The alternate "canonical atoms" implementation is used by default, and also if the `-canonical-idents` option is given. - The original implementation is used if the `-short-idents` option is given. Closes: #222 Closes: #311
| | * | Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+196
| | | | | | | | | | | | | | | | | | | | | | | | The Commandline module is reusable in other projects, and its license (GPL) allows such reuse, so its natural place is in lib/ rather than in driver/
| | * | Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
| | | | | | | | | | | | | | | | | | | | So as not to depend on an implicit import from module Program. (See PR #352.)
| | * | Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
| | | | | | | | | | | | | | | | | | | | | | | | On some versions of Coq, "nil" is of type "Rlist"... This reverts commit f070949a7559675af3e551e16e5cae95af5d4285.
| | * | Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
| | | | | | | | | | | | | | | | | | | | The rest of the code base uses `nil`, so let's be consistent. Also, this avoids depending on `Import ListNotations`.
* | | | Merge branch 'kvx-test-prepass' of ↵David Monniaux2020-11-2718-0/+1802
|\ \ \ \ | | |_|/ | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64-prepass+postpass
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-191-10/+53
| |\ \ \ | |/ / / |/| | |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-0/+6
| |\| |
| * | | fix issue 210 in simu_checkSylvain Boulmé2020-09-211-4/+10
| | | |
| * | | starting to move common filesDavid Monniaux2020-09-1616-0/+1651
| | | |
* | | | Proof of UnionFind.pathlen_unionSylvain Boulmé2020-11-161-10/+53
| |/ / |/| | | | | | | | helps to understand the difference between union and merge in the interface
* | | centralize if_sameDavid Monniaux2020-10-091-0/+6
|/ /
* | Adding copyrightsCyril SIX2020-05-044-0/+48
| |
* | moved to extraDavid Monniaux2020-04-161-0/+0
| |
* | gmap2_idemDavid Monniaux2020-04-161-65/+111
| |
* | gmap2_idemDavid Monniaux2020-04-161-0/+16
| |
* | gmap2_idem_EmptyDavid Monniaux2020-04-161-0/+54
| |
* | begin HashedMapsDavid Monniaux2020-04-161-0/+332
| |
* | forward_move_lDavid Monniaux2020-03-101-1/+13
| |
* | kill_reg_soundDavid Monniaux2020-03-091-1/+1
| |
* | CSE3 generate lists of killableDavid Monniaux2020-03-051-0/+4
| |
* | more about extraction and linkingDavid Monniaux2020-03-051-185/+180
| |
* | streamlined lattice codeDavid Monniaux2020-03-052-30/+15
| |
* | HashedSet with extractionDavid Monniaux2020-03-051-0/+6
| |
* | HashedSet with module typesDavid Monniaux2020-03-051-0/+115
| |
* | move lattice stuff where it belongsDavid Monniaux2020-03-054-0/+1446
| |
* | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-033-96/+317
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-081-4/+5
| |\| | | | | | | | | | mppa-work-upstream-merge
| * | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-1/+178
| |\ \
| | * | shrx'1_shr'David Monniaux2020-01-141-1/+127
| | | |
generated by cgit (git 2.34.1) at 2024-07-04 00:30:23 +0000