diem / move

Home of the Move programming language
Apache License 2.0
346 stars 131 forks source link

[move-prover] Add missing location line in error trace #297_163 #468

Closed satyamacn closed 1 year ago

satyamacn commented 1 year ago

Motivation

The Move prover does not print the correct line number in some error traces. Consider the example below.

public fun test_loop(x: u64) {
    if (x != 0) {
        x = 1;
    }
    else {
        x = 2;
    };
    spec {
        assert x == 1;
    };
}

The following error trace is given.

error: unknown assertion failed
  ┌─ ./sources/loop.move:9:9
  │
9 │         assert x == 1;
  │         ^^^^^^^^^^^^^^
  │
  =     at ./sources/loop.move:1: test_loop
  =         x = 0
  =     at ./sources/loop.move:2: test_loop
  =         x = 2
  =     at ./sources/loop.move:8: test_loop
  =     at ./sources/loop.move:9: test_loop

However, the assignment x = 2 occurs at Line 6 rather than Line 2. This pull request will insert at ./sources/loop.move:6: test_loop above x = 2.

Test Plan

cargo test --release

sahithiacn commented 1 year ago

/canary

bors-diem commented 1 year ago

:sunny: Canary successful

sahithiacn commented 1 year ago

/land

bors-diem commented 1 year ago

:broken_heart: Test Failed - ci-test

sahithiacn commented 1 year ago

/land