Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Symbol Table Error When Using "--race-check" in goto-instrument with CBMC for Global Array #8402

Open
ks4414 opened this issue Aug 6, 2024 · 0 comments

Comments

@ks4414
Copy link

ks4414 commented Aug 6, 2024

CBMC version: 6.0.1
Operating system: ubuntsu22.04
Exact command line resulting in the issue: See below
What behaviour did you expect: It works
What happened instead: symbol table error

When I run goto-instrument with the following source code as input, I get the following error.

test.c

#include <stdio.h>  
  
int globalArray[5];  
  
void initializeArray();  
void updateArray(int index, int newValue);  
  
void initializeArray() {  
    for (int i = 0; i < 5; i++) {  
        globalArray[i] = i + 1; 
    }  
}  
  
void updateArray(int index, int newValue) {  
    if (index >= 0 && index < 5) {  
        globalArray[index] = newValue;  
    } else {  
        printf("Index out of bounds\n");  
    }  
}  

int main() {  
    // Initialize the array  
    initializeArray();  
  
    // Update the array at a specific index  
    updateArray(2, 10); // Change the value at index 2 to 10
  
    return 0;  
}  

command

goto-cc -o test.goto test.c
goto-instrument  --race-check test.goto

result

Reading GOTO program from 'test.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Pointer Analysis
Adding Race Checks
--- begin invariant violation report ---
Invariant check failed
File: ../src/util/symbol_table_base.h:108 function: lookup_ref
Condition: symbol
Reason: `globalArray[]' must exist in the symbol table.
Backtrace:
goto-instrument(+0x8cf1e2) [0x5597440fd1e2]
goto-instrument(+0x8cff5d) [0x5597440fdf5d]
goto-instrument(+0x11fdf2) [0x55974394ddf2]
goto-instrument(+0x18f0b4) [0x5597439bd0b4]
goto-instrument(+0x1900fa) [0x5597439be0fa]
goto-instrument(+0x191e8f) [0x5597439bfe8f]
goto-instrument(+0x12648f) [0x55974395448f]
goto-instrument(+0x12962e) [0x55974395762e]
goto-instrument(+0x11db7f) [0x55974394bb7f]
goto-instrument(+0x10e566) [0x55974393c566]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7f189a666d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7f189a666e40]
goto-instrument(+0x11f3e5) [0x55974394d3e5]


--- end invariant violation report ---
Aborted
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant