Commits

Branch selector

 master

User selector

xavierleroy

Datepicker

All time

Commit History

Commits on Oct 30, 2024

• Simplify make documentation

  Show description for 044cfbc
  xavierleroy

  committed
  044cfbc

• Don't include export/ in DIRS if clightgen is not built

  Show description for aee355d
  xavierleroy

  committed
  aee355d

Commits on Oct 26, 2024

• Build .glob files at the default place and install them (AbsInt#529)

  Show description for 6da3547
  xavierleroy

  authored
  6da3547

Commits on Oct 22, 2024

• Add minimal syntactic support for type _Float16 (AbsInt#525)

  Show description for a735bfb
  xavierleroy

  authored
  a735bfb

Commits on Oct 7, 2024

• Check that preprocessed source do not contain backslash-newline

  Show description for 96e86f2
  xavierleroy

  committed
  96e86f2

Commits on Sep 29, 2024

• Enable testing Thumb-2 mode on ARMv7

  Show description for 1eb3496
  xavierleroy

  committed
  1eb3496

• Add missing dependency on $(ARCH)/sysdeps.h

  xavierleroy

  committed
  45a140b

• ARM: add and use macros for 64-bit arithmetic over register pairs

  xavierleroy

  committed
  59831be

• ARM i64_udivmod: reduce number of instructions and number of iterations

  xavierleroy

  committed
  8a3a2c0

Commits on Sep 11, 2024

• Coq 8.20.0 is supported

  xavierleroy

  committed
  20a5b48

• Update vendored MenhirLib to version 20240715

  Show description for 820fbc5
  xavierleroy

  committed
  820fbc5

Commits on Sep 10, 2024

• runtime: finish preprocessing for PowerPC assembly files

  Show description for 9129970
  xavierleroy

  committed
  9129970

• runtime: get ready to preprocess the PowerPC assembly files

  Show description for 125c493
  xavierleroy

  committed
  125c493

Commits on Sep 9, 2024

• Return Btop for undefined pointer comparisons in non-strict mode

  Show description for 7dccd5f
  xavierleroy

  committed
  7dccd5f

• Improve value analysis for mods

  Show description for 88ca6f4
  xavierleroy

  committed
  88ca6f4

• Improve value analysis for divu and divs

  Show description for c88602b
  xavierleroy

  committed
  c88602b

• Improve value analysis for mulhs, continued

  Show description for 13f84fc
  xavierleroy

  committed
  13f84fc

• ValueDomain: introduce and use urange and srange

  Show description for 068cfd8
  xavierleroy

  committed
  068cfd8

Commits on Sep 3, 2024

• Zbits: add lemmas for some useful proofs from ValueDomain

  xavierleroy

  committed
  9e19a95

Commits on Sep 2, 2024

• Value analysis: reduce Uns p 0 to IU Int.zero

  Show description for 18ecb24
  xavierleroy

  committed
  18ecb24

• Improve value analysis of mul, continued

  Show description for 6bed212
  xavierleroy

  committed
  6bed212

• Mark stack as non-executable in binaries produced by ccomp

  Show description for 82ef885
  xavierleroy

  committed
  82ef885

Commits on Aug 30, 2024

• Support Coq 8.19.2

  xavierleroy

  committed
  facbe11

Commits on Aug 26, 2024

• CombineOp: optimize (x ^ n) != 0 into x != n

  Show description for bd3813f
  xavierleroy

  committed
  bd3813f

Commits on Aug 22, 2024

• Merge pull request AbsInt#520 from AbsInt/value-analysis-IU

  Show description for d351f4b
  xavierleroy

  authored
  d351f4b

• Selection: refined heuristic for if-conversion

  Show description for af83e9a
  xavierleroy

  committed
  af83e9a

• Selection: keep track of continuation statement in sel_stmt

  Show description for eb0fb96
  xavierleroy

  committed
  eb0fb96

• Bound the recursion depth of size_stmt (AbsInt#519)

  Show description for 8ce7997
  xavierleroy

  authored
  8ce7997

Commits on Aug 21, 2024

• Constant propagation: optimize "known integer or Vundef" results

  Show description for f3f1dc2
  xavierleroy

  committed
  f3f1dc2

• Value analysis: add IU ("known integer or Vundef") static value

  Show description for 57a630c
  xavierleroy

  committed
  57a630c

Commits on Aug 20, 2024

• GHA CI: use qemu-user from backports

  Show description for 0ffc516
  xavierleroy

  committed
  0ffc516

• Update test suite

  xavierleroy

  committed
  4de5b3b

Commits on Aug 19, 2024

• GHA CI: also skip ARM testing temporarily

  Show description for 406ae8b
  xavierleroy

  committed
  406ae8b

• Compatibility with older versions of Coq

  xavierleroy

  committed
  90418d0

• Fix name of CI job

  xavierleroy

  committed
  5abe128

Pagination

PreviousNext