Skip to content

ESBMC 7.4 crashes with multi-property #1599

@tihanyin

Description

@tihanyin

In ESBMC 7.4 the following command is working:

./esbmc FormAI_44405.c --unwind 1 --overflow --no-unwinding-assertions

OUTPUT:

State 2 file FormAI_44405.c line 17 column 5 function main thread 0
----------------------------------------------------
Violated property:
  file FormAI_44405.c line 17 column 5 function main
  buffer overflow on scanf
  0


VERIFICATION FAILED

However with the same program using multi-property is crashing:
./esbmc FormAI_44405.c --unwind 1 --overflow --no-unwinding-assertions --multi-property

OUTPUT:

No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Segmentation fault (core dumped

The program is:

//FormAI DATASET v1.0 Category: Expense Tracker ; Style: peaceful
#include<stdio.h>
#include<stdlib.h>
#include<string.h>

#define MAX_SIZE 100

struct expenses{
    char category[MAX_SIZE];
    float amount;
};

int main(){
    int n;
    float total_amount = 0;
    printf("Enter the number of expenses: ");
    scanf("%d", &n);
    struct expenses e[n]; // Creating an array of n expenses

    // Taking input from user
    for(int i=0; i<n; i++){
        printf("Enter category for expense %d: ", i+1);
        scanf("%s", e[i].category);
        printf("Enter amount for expense %d: ", i+1);
        scanf("%f", &e[i].amount);
        total_amount += e[i].amount;
    }

    // Printing table header
    printf("\nCATEGORY\tAMOUNT\n");
    printf("-----------------------\n");

    // Printing expenses and their amount
    for(int i=0; i<n; i++){
        printf("%s\t\t%.2f\n", e[i].category, e[i].amount);
    }

    // Printing total expenses
    printf("\nTotal Expenses: %.2f\n", total_amount);

    return 0;
}

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions