Commits

Branch selector

 main

User selector

meng-xu-cs

Datepicker

All time

Commit History

Commits on Feb 18, 2023

• [move-prover] address comments on the boogie natives

  meng-xu-cs

  committed
  e4fa6bc

  Copy full SHA for e4fa6bc

• [move-prover] allow multiple type insts to pass through template

  meng-xu-cs

  committed
  3b7543b

  Copy full SHA for 3b7543b

• [move-prover] special case custom borrow natives in analysis

  meng-xu-cs

  committed
  8ddfb7c

  Copy full SHA for 8ddfb7c

• [move-prover] use custom borrow annotation for regular move functions

  meng-xu-cs

  committed
  18f3b07

  Copy full SHA for 18f3b07

Commits on Feb 16, 2023

• fixup! [move-prover] table intrinsic: bug fix and new intrinsic function

  meng-xu-cs

  committed
  47fca2d

  Copy full SHA for 47fca2d

• [move-prover] table intrinsic: bug fix and new intrinsic function

  Show description for b9f3e7e
  meng-xu-cs

  committed
  b9f3e7e

  Copy full SHA for b9f3e7e

Commits on Feb 6, 2023

• [move-prover] collect types in write-back chain for mono analysis

  Show description for 4901410
  meng-xu-cs

  committed
  4901410

  Copy full SHA for 4901410

Commits on Jan 22, 2023

• [move-prover] special casing havoc in reach-def annalysis

  Show description for 61b3aa7
  meng-xu-cs

  committed
  61b3aa7

  Copy full SHA for 61b3aa7

Commits on Jan 19, 2023

• fixup! [move-prover] model type_name::get in stdlib

  meng-xu-cs

  committed
  867b0bc

  Copy full SHA for 867b0bc

• [move-prover] model type_name::get in stdlib

  Show description for 7e060fd
  meng-xu-cs

  committed
  7e060fd

  Copy full SHA for 7e060fd

Commits on Jan 17, 2023

• [move-prover] check data invariants for a &mut param ...

  Show description for b4406fd
  meng-xu-cs

  committed
  b4406fd

  Copy full SHA for b4406fd

Commits on Jan 6, 2023

• fixup! fixup! [move-prover] data invariant assume and assertion for &mut params

  meng-xu-cs

  committed
  7742d4d

  Copy full SHA for 7742d4d

• fixup! [move-prover] data invariant assume and assertion for &mut params

  meng-xu-cs

  committed
  83db9ea

  Copy full SHA for 83db9ea

• [move-prover] data invariant assume and assertion for &mut params

  Show description for a7c3345
  meng-xu-cs

  committed
  a7c3345

  Copy full SHA for a7c3345

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

Pagination

Previous

Next