<commit_before>#include "stdlib.h"
#include <assert.h>

struct account {
    int balance;
    int limit;
};
typedef struct account account_t;

/*@ predicate account_pred(account_t* the_account, int the_balance, int the_limit)
    = the_account->balance |-> the_balance &*& the_account->limit |-> the_limit
    &*& malloc_block_account(the_account);
@*/

account_t* create_account(int limit)
    //@ requires limit <= 0;
    /*@ ensures  result->balance |-> 0 &*& result->limit |-> limit
        &*& malloc_block_account(result); @*/
{
    account_t* the_account = malloc(sizeof(account_t));
    if (!the_account) abort();
    the_account->balance = 0;
    the_account->limit = limit;

    return the_account;
}

int account_get_balance(account_t* my_account)
    //@ requires my_account->balance |-> ?the_balance;
    //@ ensures  my_account->balance |-> the_balance &*& result == the_balance;
{
    return my_account->balance;
}

void account_deposit(account_t* my_account, int amount)
    //@ requires account_pred(my_account, ?balance, ?limit) &*& 0 <= amount;
    //@ ensures  account_pred(my_account, balance + amount, limit);
{
    //@ open  account_pred(my_account, balance, limit);
    my_account->balance += amount;
    //@ close account_pred(my_account, balance + amount, limit);
}

int account_withdraw(account_t* my_account, int amount)
    /*@ requires my_account->limit |-> ?limit &*& my_account->balance |-> ?balance
        &*& 0 <= amount; @*/
    /*@ ensures  my_account->limit |-> limit &*& my_account->balance |-> balance - result
        &*& result == (balance - amount < limit ? balance - limit : amount); @*/
{
    int withdrawal_amount = my_account->balance - amount < my_account->limit ?
        my_account->balance - my_account->limit : amount;
    my_account->balance -= withdrawal_amount;

    return withdrawal_amount;
}

void dispose_account(account_t* my_account)
    /*@ requires my_account->balance |-> _ &*& my_account->limit |-> _
        &*& malloc_block_account(my_account); @*/
    //@ ensures  true;
{
    free(my_account);
}

int main()
    //@ requires true;<commit_msg>predicate.c fix indents<commit_after>#include "stdlib.h"
#include <assert.h>

struct account {
    int balance;
    int limit;
};
typedef struct account account_t;

/*@
predicate account_pred(account_t* the_account, int the_balance, int the_limit) =
    the_account->balance |-> the_balance &*& the_account->limit |-> the_limit &*&
    malloc_block_account(the_account);
@*/

account_t* create_account(int limit)
    //@ requires limit <= 0;
    /*@ ensures  result->balance |-> 0 &*& result->limit |-> limit &*&
            malloc_block_account(result); @*/
{
    account_t* the_account = malloc(sizeof(account_t));
    if (!the_account) abort();
    the_account->balance = 0;
    the_account->limit = limit;

    return the_account;
}

int account_get_balance(account_t* my_account)
    //@ requires my_account->balance |-> ?the_balance;
    //@ ensures  my_account->balance |-> the_balance &*& result == the_balance;
{
    return my_account->balance;
}

void account_deposit(account_t* my_account, int amount)
    //@ requires 0 <= amount &*& account_pred(my_account, ?balance, ?limit);
    //@ ensures  account_pred(my_account, balance + amount, limit);
{
    //@ open  account_pred(my_account, balance, limit);
    my_account->balance += amount;
    //@ close account_pred(my_account, balance + amount, limit);
}

int account_withdraw(account_t* my_account, int amount)
    /*@ requires 0 <= amount &*&
            my_account->limit |-> ?limit &*& my_account->balance |-> ?balance; @*/
    /*@ ensures  my_account->limit |-> limit &*& my_account->balance |-> balance - result &*&
            result == (balance - amount < limit ? balance - limit : amount); @*/
{
    int withdrawal_amount = my_account->balance - amount < my_account->limit ?
        my_account->balance - my_account->limit : amount;
    my_account->balance -= withdrawal_amount;

    return withdrawal_amount;
}

void dispose_account(account_t* my_account)
    /*@ requires my_account->balance |-> _ &*& my_account->limit |-> _ &*&
            malloc_block_account(my_account); @*/
    //@ ensures  true;
{
    free(my_account);
}

int main()
    //@ requires true;
{'fraction_non_alphanumeric': 0.150894538606403, 'fraction_numerical': 0.0023540489642184556, 'mean_word_length': 3.529850746268657, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 71, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1038032', 'n_tokens_mistral': 1395, 'n_tokens_neox': 1360, 'n_words': 283}