vampire-sys 0.5.2

Low-level FFI bindings to the Vampire theorem prover (use the 'vampire' crate instead)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

/*
 * This file is part of the source code of the software program
 * Vampire. It is protected by applicable
 * copyright laws.
 *
 * This source code is distributed under the licence found here
 * https://vprover.github.io/license.html
 * and in the source directory
 */

#include "Debug/Assertion.hpp"
#include "Lib/Deque.hpp"
#include "Test/UnitTesting.hpp"

TEST_FUN(push_front_pop_back_expand)
{
  Lib::Deque<int> *a_deque = new Lib::Deque<int>(2);
  a_deque->push_front(0);
  ASS_EQ(a_deque->pop_back(), 0);
  // push front until capacity expand
  a_deque->push_front(1);
  a_deque->push_front(2);
  // push back until capacity expand
  a_deque->push_back(3);
  a_deque->push_back(4);
  ASS_EQ(a_deque->size(), 4);
}

TEST_FUN(size_reset_desctructor)
{
  Lib::Deque<int> *a_deque = new Lib::Deque<int>();
  a_deque->push_front(1);
  a_deque->reset();
  ASS_EQ(a_deque->size(), 0);
  a_deque->push_front(1);
  // gcov sometimes misses implicitly called destructor
  a_deque->~Deque();
}