Closed
Description
#include <iostream>
#include <vector>
#include <string>
#include <algorithm>
#include <cassert>
class Car {
public:
std::string brand;
int speed;
Car(std::string brand, int speed) : brand(brand), speed(speed) {}
};
bool compare_speed(const Car& c1, const Car& c2) {
return c1.speed < c2.speed;
}
int main() {
std::vector<Car> cars = {
Car("Toyota", 120),
Car("Honda", 130),
Car("Ford", 110)
};
std::vector<Car> sorted_cars = cars;
std::sort(sorted_cars.begin(), sorted_cars.end(), compare_speed);
assert(std::is_sorted(sorted_cars.begin(), sorted_cars.end(), compare_speed) && "List is not sorted correctly!");
std::cout << "All assertions passed successfully!" << std::endl;
return 0;
}$ esbmc lambda.cpp
ESBMC version 7.8.1 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing lambda.cpp
lambda.cpp:29:17: error: no member named 'is_sorted' in namespace 'std'
assert(std::is_sorted(sorted_cars.begin(), sorted_cars.end(), compare_speed) && "List is not sorted correctly!");
~~~~~^
/usr/include/assert.h:93:27: note: expanded from macro 'assert'
(static_cast <bool> (expr) \
^~~~
In file included from lambda.cpp:2:
/tmp/esbmc-cpp-headers-7e76-c904-cc50/vector:202:15: error: no matching constructor for initialization of 'Car[]'
buf = new T[init.size()];
^
lambda.cpp:20:29: note: in instantiation of member function 'std::vector<Car>::vector' requested here
std::vector<Car> cars = {
^
lambda.cpp:7:7: note: candidate constructor (the implicit move constructor) not viable: requires 1 argument, but 0 were provided
class Car {
^
lambda.cpp:7:7: note: candidate constructor (the implicit copy constructor) not viable: requires 1 argument, but 0 were provided
lambda.cpp:12:5: note: candidate constructor not viable: requires 2 arguments, but 0 were provided
Car(std::string brand, int speed) : brand(brand), speed(speed) {}
^
In file included from lambda.cpp:2:
/tmp/esbmc-cpp-headers-7e76-c904-cc50/vector:192:15: error: no matching constructor for initialization of 'Car[]'
buf = new T[x._size];
^
lambda.cpp:26:36: note: in instantiation of member function 'std::vector<Car>::vector' requested here
std::vector<Car> sorted_cars = cars;
^
lambda.cpp:7:7: note: candidate constructor (the implicit move constructor) not viable: requires 1 argument, but 0 were provided
class Car {
^
lambda.cpp:7:7: note: candidate constructor (the implicit cop
5447
y constructor) not viable: requires 1 argument, but 0 were provided
lambda.cpp:12:5: note: candidate constructor not viable: requires 2 arguments, but 0 were provided
Car(std::string brand, int speed) : brand(brand), speed(speed) {}
^
ERROR: PARSING ERROR