Commits

Branch selector

 master

User selector

All users

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

• ARM runtime: fix typo in header file

  Show description for bf8a3e1
  

  bschommer

  authored and

  xavierleroy

  committed
  bf8a3e1

Commits on Oct 21, 2024

• install .v files alongside .vo files (AbsInt#527)

  JasonGross

  authored
  29dfd42

Commits on Oct 7, 2024

• Check that preprocessed source do not contain backslash-newline

  Show description for 96e86f2
  xavierleroy

  committed
  96e86f2

Commits on Oct 3, 2024

• Adapt to coq/coq#19530 (AbsInt#524)

  Show description for 5f90f91
  proux01

  authored
  5f90f91

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

• Add missing temp_env parameter to documentation of Clight.eval_expr (AbsInt#523)

  

  ebresafegaga

  authored and

  xavierleroy

  committed
  7bd609f

• 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

• Improve value analysis for mulhs

  Show description for 7913dfe
  

  bschommer

  authored and

  xavierleroy

  committed
  7913dfe

• Improve value analysis result for mulhu

  Show description for 3d8aebf
  

  bschommer

  and

  xavierleroy

  committed
  3d8aebf

• Zbits: add lemmas for some useful proofs from ValueDomain

  xavierleroy

  committed
  9e19a95

• Some properties about two_p, mulhu and mulhs.

  

  bschommer

  authored and

  xavierleroy

  committed
  0775627

Commits on Sep 2, 2024

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

  Show description for 18ecb24
  xavierleroy

  committed
  18ecb24

• Value analysis for divu, divs, modu, mods: add missing IU cases

  

  bschommer

  authored and

  xavierleroy

  committed
  b1f0f6a

• Improve value analysis of mul, continued

  Show description for 6bed212
  xavierleroy

  committed
  6bed212

• Improve value analysis of mul.

  Show description for bdabdcc
  

  bschommer

  and

  xavierleroy

  committed
  bdabdcc

• 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 25, 2024

• Merge pull request AbsInt#521 from ebresafegaga/patch-1

  Show description for 7c87292
  m-schmidt

  authored
  7c87292

Commits on Aug 24, 2024

• Mgetparent -> Mgetparam

  ebresafegaga

  authored
  9256ae5

Pagination

PreviousNext