Commits

Branch selector

 main

User selector

meng-xu-cs

Datepicker

All time

Commit History

Commits on Dec 18, 2022

• [move-prover] only allow move types when computing type insts for axioms

  meng-xu-cs

  committed
  781c844

  Copy full SHA for 781c844

Commits on Dec 16, 2022

• [move-prover] explicit well-formed assumption after havoc

  Show description for 70c811f
  meng-xu-cs

  committed
  70c811f

  Copy full SHA for 70c811f

Commits on Dec 8, 2022

• [move-prover] convert borrow analysis with interprocedural absint

  Show description for 796ddf2
  meng-xu-cs

  committed
  796ddf2

  Copy full SHA for 796ddf2

• [move-prover] test case for mutually recursive functions

  meng-xu-cs

  committed
  e41ac9e

  Copy full SHA for e41ac9e

• [move-prover] do not emit error on recursive functions

  meng-xu-cs

  committed
  11df349

  Copy full SHA for 11df349

• [move-prover] propogate the scc group info into each processor

  meng-xu-cs

  committed
  451bff8

  Copy full SHA for 451bff8

• [move-prover] prepare the borrow analysis for inter-procedure absint

  Show description for 8117efe
  meng-xu-cs

  committed
  8117efe

  Copy full SHA for 8117efe

• [move-prover] allow annotations to mark whether a fixedpoint is reached

  Show description for 82193ae
  meng-xu-cs

  committed
  82193ae

  Copy full SHA for 82193ae

• [move-prover] deterministic ordering of worklist with recursive calls

  Show description for 68cc30a
  meng-xu-cs

  committed
  68cc30a

  Copy full SHA for 68cc30a

Commits on Nov 26, 2022

• fixup! [move-prover] axiom for relating table contains to length

  meng-xu-cs

  committed
  a204d67

  Copy full SHA for a204d67

• [move-prover] axiom for relating table contains to length

  Show description for 4922506
  meng-xu-cs

  committed
  4922506

  Copy full SHA for 4922506

• [move-prover] customized encoding for map equality

  Show description for c40f995
  meng-xu-cs

  committed
  c40f995

  Copy full SHA for c40f995

• [move-prover] data invariants for map values

  Show description for 22ce661
  meng-xu-cs

  committed
  22ce661

  Copy full SHA for 22ce661

Commits on Nov 24, 2022

• fixup! [move-prover] add the spec_is_struct<T> function

  meng-xu-cs

  committed
  e01d88a

  Copy full SHA for e01d88a

• [move-prover] add the spec_is_struct<T> function

  meng-xu-cs

  committed
  1e7601c

  Copy full SHA for 1e7601c

• [move-prover] better type info scheme

  Show description for bc236bd
  meng-xu-cs

  committed
  bc236bd

  Copy full SHA for bc236bd

• [extension] remove redundant intrinsic decl

  meng-xu-cs

  committed
  14f9419

  Copy full SHA for 14f9419

• [move-model] two ways to test is_intrinsic

  Show description for 29e64a5
  meng-xu-cs

  committed
  29e64a5

  Copy full SHA for 29e64a5

Commits on Sep 26, 2022

• [move-bytecode-verifier] explicitly list all bytecode in acquires pass

  Show description for 54d27fc
  meng-xu-cs

  committed
  54d27fc

  Copy full SHA for 54d27fc

Commits on Sep 19, 2022

• [move-model] do not report errors when translating a non-pure fun to spec fun (move-language#489)

  Show description for be95435
  meng-xu-cs

  authored
  be95435

  Copy full SHA for be95435

Commits on Sep 15, 2022

• [move-prover] allow recursive move function

  Show description for 1bfb1e7
  meng-xu-cs

  committed
  1bfb1e7

  Copy full SHA for 1bfb1e7

Commits on Sep 12, 2022

• [move-prover] a testcase for multiple table implementations

  meng-xu-cs

  committed
  e1d5b80

  Copy full SHA for e1d5b80

• [move-prover] fully parameterize the boogie tempalte for tables

  meng-xu-cs

  committed
  d187ce3

  Copy full SHA for d187ce3

• [move-prover] replace is_well_known on tables with is_intrinsic_of

  meng-xu-cs

  committed
  5743520

  Copy full SHA for 5743520

• [move-model] allow intrinsic suites to be declared in struct spec

  meng-xu-cs

  committed
  d795651

  Copy full SHA for d795651

• [move-model] make pragma parsing stateful

  Show description for ab7e548
  meng-xu-cs

  committed
  ab7e548

  Copy full SHA for ab7e548

Commits on Sep 10, 2022

• [move-prover] switch src/dst pair for the havoc operator (move-language#467)

  Show description for e0dafc5
  meng-xu-cs

  authored
  e0dafc5

  Copy full SHA for e0dafc5

Commits on Sep 8, 2022

• [move-prover] model type_of which returns the struct tag triple (move-language#462)

  Show description for f57c130
  meng-xu-cs

  authored
  f57c130

  Copy full SHA for f57c130

Commits on Sep 7, 2022

• [move-prover] preliminary support for type reflection (move-language#451)

  Show description for f982b26
  meng-xu-cs

  authored
  f982b26

  Copy full SHA for f982b26

Commits on Sep 1, 2022

• [move-model] re-use the address map produced by move compiler (move-language#429)

  Show description for 164bf33
  meng-xu-cs

  authored
  164bf33

  Copy full SHA for 164bf33

• [move-prover] extract plain trace from boogie error reports (move-language#430)

  Show description for d0825b3
  meng-xu-cs

  authored
  d0825b3

  Copy full SHA for d0825b3

Commits on Aug 30, 2022

• [move-compiler] implement the #[verify_only] attribute (move-language#420)

  Show description for 4a5ccd2
  meng-xu-cs

  authored
  4a5ccd2

  Copy full SHA for 4a5ccd2

Commits on Aug 6, 2022

• [move-prover] fix field type instantiation in borrow edge (move-language#350)

  meng-xu-cs

  authored
  7b24d06

  Copy full SHA for 7b24d06

Commits on Aug 3, 2022

• [move-prover] do not remap moved nodes in borrow analysis (move-language#335)

  Show description for f618b1b
  meng-xu-cs

  authored
  f618b1b

  Copy full SHA for f618b1b

Commits on Aug 1, 2022

• [move-prover][interpreter] two bug fixes to re-enable disabled tests (move-language#324)

  Show description for a3bccb0
  meng-xu-cs

  authored
  a3bccb0

  Copy full SHA for a3bccb0

Pagination

Previous

Next